p:FinProbSpace, A:(p-open(p)). countable-p-union(i.A(i))  p-open(p) 

latex

Definitions

, Outcome, x:AB(x), {i..j}, A  B, x:A. B(x), {x:A| B(x)} , t  T, FinProbSpace, #$n, Type, S  T, P & Q, i  j < k, suptype(S; T), <a, b>, f(a), x:A  B(x), x.A(x), a < b, Void, P  Q, False, A, countable-p-union(i.A(i)), p-open(p), , s = t, , b, b, , (i = j), P  Q, Unit, left + right, imax-list(L), ||as||, upto(n), x(s), map(f;as), x:A.B(x), Top, (xL.P(x)), P  Q, (x  l), x:A. B(x), type List, xL. P(x), if b then t else f fi , P  Q, Dec(P), {T}, SQType(T), s ~ t, A c B, True, T, SqStable(P)

Lemmas

sq stable from decidable, decidable le, member upto2, decidable int equal, length wf1, imax-list-lb, member map, member upto, l member wf, imax-list-ub, length-map, length upto, imax-list wf, map wf, upto wf, eqtt to assert, eqff to assert, iff transitivity, assert of bnot, not functionality wrt iff, assert of eq int, eq int wf, bool wf, bnot wf, not wf, assert wf, le wf, nat wf, p-outcome wf, int seg wf, finite-prob-space wf